Matriochka - Step 2 - Nuit du Hack CTF Quals 2016

#Nuit_du_Hack_CTF_Quals_2016

Matriochka - Step 1 - Nuit du Hack CTF Quals 2016と同じようなバイナリが配布される

Ghidraに投げると以下のmain関数が得られた

code: c

void main(uint32_t argc, char **argv)

{

char cVar1;

char cVar2;

char cVar3;

char cVar4;

char cVar5;

int64_t iVar6;

char **s;

uint32_t var_24h;

uint32_t var_14h;

if (argc == 2) {

iVar6 = sym.imp.strlen(argv1);

if (((iVar6 + 1) * 0x2a == 0x1f8) &&

(cVar1 = *argv1, cVar2 = argv13, cVar3 = *argv1, cVar4 = argv16, cVar5 = argv15,

iVar6 = sym.imp.strlen(argv1),

(int32_t)argv18 - (int32_t)argv17 == 0xd &&

((int32_t)argv12 - (int32_t)argv11 == 0xd &&

(argv14 == 'i' &&

(argv13 == argv19 &&

(argv11 + -0x11 == (int32_t)*argv1 &&

(argv11 == argv110 &&

(argv11 == argv17 &&

((int64_t)cVar5 == iVar6 * 9 + -4 &&

(cVar3 + 0x10 == cVar4 + -0x10 && (((int32_t)cVar2 & 0x7fffffffU) == 100 && cVar1 == 'P'))))))))))) {

fcn.0040064d(argv1);

} else {

sym.imp.fprintf(_reloc.stdout, "Try again...\n");

}

} else {

sym.imp.fprintf(_reloc.stdout, "Usage: %s <pass>\n", *argv);

}

return;

}

文字列長は11文字

諸々の条件をz3に投げて解いてもらう

code: python

from z3 import *

args = BitVec("arg%d" % i, 8) for i in range(11)

s = Solver()

for i in range(11):

s.add(0x20 <= argsi)

s.add(argsi <= 0x7e)

s.add(args8 - args7 == 0xd)

s.add(args2 - args1 == 0xd)

s.add(args4 == ord('i'))

s.add(args3 == args9)

s.add(args1 - 0x11 == args0)

s.add(args1 == args10)

s.add(args1 == args7)

s.add(args5 == 11 * 9 - 4)

s.add(args0 + 0x10 == args6 - 0x10)

s.add(args3 == 100)

s.add(args0 == ord('P'))

r = s.check()

if r == sat:

m = s.model()

for i in range(11):

print(chr(m[argsi].as_long()), end="")

Pandi_panda